Termination w.r.t. Q proof of /tmp/tmpQy9Noq/wiehe12.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

P(s(x), x) → GT(x, x)
P(s(x), s(y)) → GT(x, y)
GT(s(x), s(y)) → GT(x, y)
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
N(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
F(s(x)) → H(x)
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
P(s(x), s(y)) → ID(x)
MINUS(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
P(s(x), s(y)) → IF(gt(x, y), x, y)
NOT(x) → IF(x, false, true)
P(s(x), s(y)) → NOT(gt(x, y))
G(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → N(s(x), s(y))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
M(s(x), s(y)) → M(x, y)
H(s(x)) → F(x)
K(s(x), s(y)) → K(minus(x, y), s(y))
P(s(x), x) → ID(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → F(s(y))
G(s(x), s(y)) → F(s(x))
K(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

P(s(x), x) → GT(x, x)
P(s(x), s(y)) → GT(x, y)
GT(s(x), s(y)) → GT(x, y)
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
N(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
F(s(x)) → H(x)
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
P(s(x), s(y)) → ID(x)
MINUS(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
P(s(x), s(y)) → IF(gt(x, y), x, y)
NOT(x) → IF(x, false, true)
P(s(x), s(y)) → NOT(gt(x, y))
G(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → N(s(x), s(y))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
M(s(x), s(y)) → M(x, y)
H(s(x)) → F(x)
K(s(x), s(y)) → K(minus(x, y), s(y))
P(s(x), x) → ID(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → F(s(y))
G(s(x), s(y)) → F(s(x))
K(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 25 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(x), s(y)) → GT(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(x), s(y)) → GT(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GT(s(x), s(y)) → GT(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → H(x)
H(s(x)) → F(x)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → H(x)
H(s(x)) → F(x)

From the DPs we obtained the following set of size-change graphs:

H(s(x)) → F(x)
The graph contains the following edges 1 > 1
F(s(x)) → H(x)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(s(x), s(y)) → MINUS(x, y)

From the DPs we obtained the following set of size-change graphs:

MINUS(s(x), s(y)) → MINUS(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))

The remaining pairs can at least be oriented weakly.

P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

Used ordering: Polynomial interpretation with max and min functions [25]:

POL(0) = 0
POL(P(x₁, x₂)) = max(x₁, x₂)
POL(false) = 0
POL(gt(x₁, x₂)) = 0
POL(id(x₁)) = x₁
POL(if(x₁, x₂, x₃)) = max(x₂, x₃)
POL(not(x₁)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following usable rules [17] were oriented:

if(true, x, y) → x
id(x) → x
if(false, x, y) → y

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))

The remaining pairs can at least be oriented weakly.

P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( if(x₁, ..., x₃) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	1	0	\
\	0	1	/

x₂

/	1	0	\
\	0	1	/

x₃

M( true ) =

/	0	\
\	0	/

M( false ) =

/	0	\
\	0	/

M( s(x₁) ) =

/	1	\
\	1	/

/	1	1	\
\	1	1	/

x₁

M( gt(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	0	/

x₁

/	1	0	\
\	0	0	/

x₂

M( id(x₁) ) =

/	1	\
\	0	/

/	1	0	\
\	0	1	/

x₁

M( 0 ) =

/	0	\
\	0	/

Tuple symbols:

M( P(x₁, x₂) ) =

[

]

x₁

[

]

x₂

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

if(true, x, y) → x
id(x) → x
if(false, x, y) → y

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation with max and min functions [25]:

POL(0) = 0
POL(P(x₁, x₂)) = x₁
POL(false) = 0
POL(gt(x₁, x₂)) = 0
POL(id(x₁)) = x₁
POL(if(x₁, x₂, x₃)) = max(x₂, x₃)
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following usable rules [17] were oriented:

if(true, x, y) → x
id(x) → x
if(false, x, y) → y

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

K(s(x), s(y)) → K(minus(x, y), s(y))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

K(s(x), s(y)) → K(minus(x, y), s(y))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(K(x₁, x₂)) = x₁
POL(minus(x₁, x₂)) = x₁
POL(s(x₁)) = 1 + x₁

The following usable rules [17] were oriented:

minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

M(s(x), s(y)) → M(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

M(s(x), s(y)) → M(x, y)

From the DPs we obtained the following set of size-change graphs:

M(s(x), s(y)) → M(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

N(s(x), s(y)) → N(x, y)

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

N(s(x), s(y)) → N(x, y)

From the DPs we obtained the following set of size-change graphs:

N(s(x), s(y)) → N(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))

The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( n(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

/	0	0	\
\	0	0	/

x₂

M( m(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

/	1	0	\
\	0	1	/

x₂

M( minus(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

/	0	0	\
\	0	0	/

x₂

M( k(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

/	0	0	\
\	0	0	/

x₂

M( s(x₁) ) =

/	1	\
\	0	/

/	1	1	\
\	1	1	/

x₁

M( 0 ) =

/	0	\
\	0	/

Tuple symbols:

M( G(x₁, x₂) ) =

[

]

x₁

[

]

x₂

n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.